E ::= n
    | x
    | f(E…)
    | let x = E in E

P ::= int | intptr[l]
C ::= P(x) | C & C | ⊤
Σ ::= l…; x… ⊢ C

Γ ::= ε | Γ,f(Σ)→Σ | Γ,y | Γ,x:=α
W ::= ε | E:W | apply[f]:W | let[x,E]:W | drop[x]:W
S ::= ε | α:S


Defn [ <Γ;C;S;W> → <Γ;C;S;W> ]

x:=y in Γ
------------
<Γ; C; S; x:W> → <Γ; C; y:S; W>

x free in Γ
------------
<Γ; C; S; n:W> → <Γ,x; C & int(x); x:S; W>

------------
<Γ; C; S; f(E…):W> → <Γ; C; S; E…:apply[f]:W>

------------
<Γ; C; S; (let x = E1 in E2):W> → <Γ; C; S; E1:bind[x]:E2:drop[x]:W>

y free in Γ
Γ ⊢ f(x…) → l…; y : C' ⇒ C"
⊢ C' ⊆ C
----------------------------------------
<Γ; C; x…:S; apply[f]:W> → <Γ,l…,y; (C & C"); y:S; W>

----------------------------------------
<Γ; C; y:S; bind[x]:W> → <Γ,x:=y; C; S; W>



f<N>(vec: Vec<A, N+1>)


let x: Vec<A, M+1>
f(x)



N + 1
M + 2

M = 1 + N
